Search results for "Two-variable logic"

showing 2 items of 2 documents

Finite Satisfiability of the Two-Variable Guarded Fragment with Transitive Guards and Related Variants

2018

We consider extensions of the two-variable guarded fragment, GF2, where distinguished binary predicates that occur only in guards are required to be interpreted in a special way (as transitive relations, equivalence relations, pre-orders or partial orders). We prove that the only fragment that retains the finite (exponential) model property is GF2 with equivalence guards without equality. For remaining fragments we show that the size of a minimal finite model is at most doubly exponential. To obtain the result we invent a strategy of building finite models that are formed from a number of multidimensional grids placed over a cylindrical surface. The construction yields a 2NExpTime-upper bou…

FOS: Computer and information sciencesComputer Science - Logic in Computer ScienceTwo-variable logicGeneral Computer ScienceComputational complexity theoryLogicguarded fragmentBinary number0102 computer and information sciences01 natural sciencesUpper and lower boundsTheoretical Computer ScienceCombinatoricstransitive relationEquivalence relationfinite satisfiability problem0101 mathematicsEquivalence (formal languages)Integer programmingMathematicsDiscrete mathematicsTransitive relationNEXPTIMEcomputational complexity010102 general mathematicsLogic in Computer Science (cs.LO)Computational Mathematics010201 computation theory & mathematicsequivalence ralationACM Transactions on Computational Logic
researchProduct

Two-variable First-Order Logic with Counting in Forests

2018

We consider an extension of two-variable, first-order logic with counting quantifiers and arbitrarily many unary and binary predicates, in which one distinguished predicate is interpreted as the mother-daughter relation in an unranked forest. We show that both the finite satisfiability and the general satisfiability problems for the extended logic are decidable in NExpTime. We also show that the decision procedure for finite satisfiability can be extended to the logic where two distinguished predicates are interpreted as the mother-daughter relations in two independent forests.

Variable (computer science)general satisfiabilityfinite satisfiabilitylogic and computational complexitydecision proceduresArithmetictwo-variable logic with counting quantifiersunranked trees/forestsMathematicsFirst-order logicEPiC Series in Computing
researchProduct